home *** CD-ROM | disk | FTP | other *** search
/ Night Owl 6 / Night Owl's Shareware - PDSI-006 - Night Owl Corp (1990).iso / 016a / gofer221.zip / TYPE.C < prev    next >
C/C++ Source or Header  |  1991-11-20  |  61KB  |  1,883 lines
  1. /* --------------------------------------------------------------------------
  2.  * type.c:    Copyright (c) Mark P Jones 1991.   All rights reserved.
  3.  *        See goferite.h for details and conditions of use etc...
  4.  *        Gofer version 2.21 November 1991
  5.  *
  6.  *        Last updated 11/11/91 mpj
  7.  *
  8.  * This is the gofer type checker:  Based on the extended algorithm in my
  9.  * PRG technical report PRG-TR-10-91, supporting the use of qualified types
  10.  * in the form of multi-parameter type classes, according to my `new
  11.  * approach' to type classes posted to the Haskell mailing list.
  12.  * This program uses the optimisations for constant and locally-constant
  13.  * overloading.
  14.  * ------------------------------------------------------------------------*/
  15.  
  16. #include "prelude.h"
  17. #include "storage.h"
  18. #include "connect.h"
  19. #include "errors.h"
  20.  
  21. Bool coerceNumLiterals = FALSE;        /* TRUE => insert fromInteger calls*/
  22.                     /*         etc for numeric literals*/
  23. Bool catchAmbigs       = FALSE;        /* TRUE => functions with ambig.   */
  24.                     /*        types produce error       */
  25.  
  26. Type typeString, typeDialogue;        /* String & Dialogue types       */
  27. Name nameTrue, nameFalse;        /* primitive boolean constructors  */
  28. Name nameNil, nameCons;            /* primitive list constructors       */
  29.  
  30. /* --------------------------------------------------------------------------
  31.  * Data structures for storing a substitution:
  32.  *
  33.  * For various reasons, this implementation uses structure sharing, instead of
  34.  * a copying approach.    In principal, this is fast and avoids the need to
  35.  * build new type expressions.    Unfortunately, this implementation will not
  36.  * be able to handle *very* large expressions.
  37.  *
  38.  * The substitution is represented by an array of type variables each of
  39.  * which is a pair:
  40.  *    bound    a (skeletal) type expression, or NIL if the variable
  41.  *        is not bound.
  42.  *    offs    offset of skeleton in bound.  If isNull(bound), then offs is
  43.  *        used to indicate whether that variable is generic (i.e. free
  44.  *        in the current assumption set) or fixed (i.e. bound in the
  45.  *        current assumption set).  Generic variables are assigned
  46.  *        offset numbers whilst copying type expressions (t,o) to
  47.  *        obtain their most general form.
  48.  * ------------------------------------------------------------------------*/
  49.  
  50. typedef struct {            /* Each type variable contains:       */
  51.     Type bound;                /* A type skeleton (unbound==NIL)  */
  52.     Int  offs;                /* Offset for skeleton           */
  53. } Tyvar;
  54.  
  55. static    Int      numTyvars;        /* no. type vars currently in use  */
  56. static    Tyvar      tyvars[NUM_TYVARS];    /* storage for type variables       */
  57. static    Int      typeOff;        /* offset of result type        */
  58. static    Type      typeIs;        /* skeleton of result type       */
  59. static    List      predsAre;        /* list of predicates in type       */
  60. #define tyvar(n)  (tyvars+(n))        /* nth type variable           */
  61. #define tyvNum(t) ((t)-tyvars)        /* and the corresp. inverse funct. */
  62. static    Int      nextGeneric;            /* number of generics found so far */
  63.  
  64.                         /* offs values when isNull(bound): */
  65. #define FIXED_TYVAR    0            /* fixed in current assumption       */
  66. #define UNUSED_GENERIC 1            /* not fixed, not yet encountered  */
  67. #define GENERIC        2            /* GENERIC+n==nth generic var found*/
  68.  
  69. /* --------------------------------------------------------------------------
  70.  * Local function prototypes:
  71.  * ------------------------------------------------------------------------*/
  72.  
  73. static Void   local emptySubstitution Args((Void));
  74. static Int    local newTyvars         Args((Int));
  75. static Tyvar *local getTypeVar        Args((Type,Int));
  76. static Void   local tyvarType         Args((Int));
  77. static Void   local bind              Args((Int,Type,Int));
  78. static Void   local expandSynonym     Args((Tycon, Type *, Int *));
  79.  
  80. static Void   local clearMarks        Args((Void));
  81. static Void   local resetGenericsFrom Args((Int));
  82. static Void   local markTyvar         Args((Int));
  83. static Void   local markType          Args((Type,Int));
  84.  
  85. static Type   local copyTyvar         Args((Int));
  86. static Type   local copyType          Args((Type,Int));
  87.  
  88. static Bool   local doesntOccurIn     Args((Type,Int));
  89.  
  90. static Bool   local varToVarBind      Args((Tyvar *,Tyvar *));
  91. static Bool   local varToTypeBind     Args((Tyvar *,Type,Int));
  92. static Bool   local unify             Args((Type,Int,Type,Int));
  93. static Bool   local sameType          Args((Type,Int,Type,Int));
  94.  
  95. static Void   local emptyAssumption   Args((Void));
  96. static Void   local enterBindings     Args((Void));
  97. static Void   local leaveBindings     Args((Void));
  98. static Void   local markAssumList     Args((List));
  99. static Cell   local findAssum         Args((Text));
  100. static Pair   local findInAssumList   Args((Text,List));
  101. static Int    local newVarsBind       Args((Cell));
  102. static Void   local newDefnBind       Args((Cell,Type));
  103. static Void   local instantiate       Args((Type));
  104.  
  105. static Void   local typeError         Args((Int,Cell,Cell,String,Type,Int));
  106. static Cell   local typeExpr          Args((Int,Cell));
  107. static Cell   local varIntro          Args((Cell,Type));
  108. static Void   local typeEsign         Args((Int,Cell));
  109. static Void   local typeCase          Args((Int,Int,Cell));
  110. static Void   local typeQualifier     Args((Int,Cell));
  111. static Cell   local typeFreshPat      Args((Int,Cell));
  112.  
  113. static Cell   local typeAp            Args((Int,Cell));
  114. static Void   local typeAlt           Args((Cell));
  115. static Int    local funcType          Args((Int));
  116.  
  117. static Void   local typeTuple         Args((Cell));
  118. static Type   local makeTupleType     Args((Int));
  119.  
  120. static Void   local typeBindings      Args((List));
  121. static Void   local removeTypeSigs    Args((Cell));
  122.  
  123. static Void   local noOverloading     Args((List));
  124. static Void   local restrictedBindAss Args((Cell));
  125. static Void   local restrictedAss     Args((Int,Cell,Type));
  126.  
  127. static Void   local explicitTyping    Args((List));
  128. static List   local gotoExplicit      Args((List));
  129. static List   local explPreds         Args((Text,List,List));
  130.  
  131. static Void   local implicitTyping    Args((List));
  132. static Void   local addEvidParams     Args((List,Cell));
  133.  
  134. static Void   local typeInstDefn      Args((Inst));
  135. static Void   local typeClassDefn     Args((Class));
  136. static Void   local typeMembers       Args((String,List,List,Cell,Int));
  137. static Void   local typeMember        Args((String,Name,Name,Cell,Int));
  138.  
  139. static Void   local typeBind          Args((Cell));
  140. static Void   local typeDefAlt        Args((Int,Cell,Pair));
  141. static Cell   local typeRhs           Args((Cell));
  142. static Void   local guardedType       Args((Int,Cell));
  143.  
  144. static Void   local generaliseBind    Args((Int,List,Cell));
  145. static Void   local generaliseAss     Args((Int,List,Cell));
  146. static Type   local generalise        Args((List,Type));
  147.  
  148. static Void   local checkBindSigs     Args((Cell));
  149. static Void   local checkTypeSig      Args((Int,Cell,Type));
  150. static Void   local tooGeneral        Args((Int,Cell,Type,Type));
  151.  
  152. static Bool   local equalSchemes      Args((Type,Type));
  153. static Bool   local equalQuals        Args((List,List));
  154. static Bool   local equalTypes        Args((Type,Type));
  155.  
  156. static Void   local typeDefnGroup     Args((List));
  157.  
  158. /* --------------------------------------------------------------------------
  159.  * Frequently used type skeletons:
  160.  * ------------------------------------------------------------------------*/
  161.  
  162. static Type  var;            /* mkOffset(0)                  */
  163. static Type  arrow;            /* mkOffset(0) -> mkOffset(1)      */
  164. static Type  typeList;            /* [ mkOffset(0) ]                */
  165. static Type  typeBool;            /* Bool                      */
  166. static Type  typeInt;            /* Int (or Num)               */
  167. static Type  typeFloat;                /* Float                           */
  168. static Type  typeUnit;            /* ()                   */
  169. static Type  typeChar;            /* Char                      */
  170. static Type  typeIntToInt;        /* Int -> Int                  */
  171.  
  172. static Name  nameFromInt;        /* fromInteger function           */
  173. static Class classNum;            /* class Num               */
  174. static Cell  predNum;            /* Num (mkOffset(0))           */
  175.  
  176. /* --------------------------------------------------------------------------
  177.  * Basic operations on current substitution:
  178.  * ------------------------------------------------------------------------*/
  179.  
  180. static Void local emptySubstitution() {    /* clear current substitution       */
  181.     numTyvars   = 0;
  182.     nextGeneric = 0;
  183.     typeIs      = NIL;
  184.     predsAre    = NIL;
  185. }
  186.  
  187. static Int local newTyvars(n)            /* allocate new type variables       */
  188. Int n; {
  189.     Int beta = numTyvars;
  190.  
  191.     if (numTyvars+n>NUM_TYVARS) {
  192.     ERROR(0) "Too many type variables in type checker"
  193.     EEND;
  194.     }
  195.     for (numTyvars+=n; n>0; n--) {
  196.     tyvars[numTyvars-n].offs  = UNUSED_GENERIC;
  197.     tyvars[numTyvars-n].bound = NIL;
  198.     }
  199.     return beta;
  200. }
  201.  
  202. #define freeTypeVars(beta) numTyvars=beta
  203.  
  204. #define deRef(tyv,t,o)  while ((tyv=getTypeVar(t,o)) && tyv->bound) { \
  205.                             t = tyv->bound;                           \
  206.                             o = tyv->offs;                            \
  207.                         }
  208.  
  209. static Tyvar *local getTypeVar(t,o)    /* get number of type variable       */
  210. Type t;                 /* represented by (t,o) [if any].  */
  211. Int  o; {
  212.     switch (whatIs(t)) {
  213.     case INTCELL : return tyvar(intOf(t));
  214.     case OFFSET  : return tyvar(o+offsetOf(t));
  215.     }
  216.     return ((Tyvar *)0);
  217. }
  218.  
  219. static Void local tyvarType(vn)           /* load type held in type variable */
  220. Int vn; {                       /* vn into (typeIs,typeOff)       */
  221.     Tyvar *tyv;
  222.  
  223.     while ((tyv=tyvar(vn))->bound)
  224.     switch(whatIs(tyv->bound)) {
  225.         case INTCELL : vn = intOf(tyv->bound);
  226.                break;
  227.  
  228.         case OFFSET  : vn = offsetOf(tyv->bound)+(tyv->offs);
  229.                break;
  230.  
  231.         default     : typeIs  = tyv->bound;
  232.                typeOff = tyv->offs;
  233.                return;
  234.     }
  235.     typeIs  = var;
  236.     typeOff = vn;
  237. }
  238.  
  239. static Void local bind(vn,t,o)               /* set type variable vn to (t,o)   */
  240. Int  vn;
  241. Type t;
  242. Int  o; {
  243.     Tyvar *tyv = tyvar(vn);
  244.     tyv->bound = t;
  245.     tyv->offs  = o;
  246. }
  247.  
  248. static Void local expandSynonym(h,at,ao)/* Expand type synonym with head h */
  249. Tycon h;                 /* original expression (*at,*ao)   */
  250. Type  *at;                    /* expansion returned in (*at,*ao) */
  251. Int   *ao; {
  252.     Int  n = tycon(h).arity;
  253.     Type t = *at;
  254.     Int  o = *ao;
  255.  
  256.     *at = tycon(h).defn;
  257.     *ao = newTyvars(n);
  258.     for (; 0<n--; t=fun(t))
  259.     bind(*ao+n,arg(t),o);
  260. }
  261.  
  262. /* --------------------------------------------------------------------------
  263.  * Mark type expression, so that all variables are marked as unused generics
  264.  * ------------------------------------------------------------------------*/
  265.  
  266. static Void local clearMarks() {           /* set all unbound type vars to       */
  267.     Int i;                       /* unused generic variables       */
  268.     for (i=0; i<numTyvars; ++i)
  269.     if (isNull(tyvars[i].bound))
  270.         tyvars[i].offs = UNUSED_GENERIC;
  271.     nextGeneric = 0;
  272. }
  273.  
  274. static Void local resetGenericsFrom(n)    /* reset all generic vars to unused*/
  275. Int n; {                /* for generics >= n           */
  276.     Int i;
  277.     for (i=0; i<numTyvars; ++i)
  278.     if (isNull(tyvars[i].bound) && tyvars[i].offs>=GENERIC+n)
  279.         tyvars[i].offs = UNUSED_GENERIC;
  280.     nextGeneric = n;
  281. }
  282.  
  283. static Void local markTyvar(vn)            /* mark fixed vars in type bound to*/
  284. Int vn; {                       /* given type variable           */
  285.     Tyvar *tyv = tyvar(vn);
  286.  
  287.     if (tyv->bound)
  288.     markType(tyv->bound, tyv->offs);
  289.     else
  290.     (tyv->offs) = FIXED_TYVAR;
  291. }
  292.  
  293. static Void local markType(t,o)            /* mark fixed vars in type (t,o)   */
  294. Type t;
  295. Int  o; {
  296.     switch (whatIs(t)) {
  297.     case TYCON   :
  298.     case TUPLE   :
  299.     case UNIT    :
  300.     case ARROW   :
  301.     case LIST    : return;
  302.  
  303.     case AP      : markType(fst(t),o);
  304.                markType(snd(t),o);
  305.                return;
  306.  
  307.     case OFFSET  : markTyvar(o+offsetOf(t));
  308.                return;
  309.  
  310.     case INTCELL : markTyvar(intOf(t));
  311.                return;
  312.  
  313.     default      : internal("markType");
  314.     }
  315. }
  316.  
  317. /* --------------------------------------------------------------------------
  318.  * Copy type expression from substitution to make a single type expression:
  319.  * ------------------------------------------------------------------------*/
  320.  
  321. static Type local copyTyvar(vn)            /* calculate most general form of  */
  322. Int vn; {                       /* type bound to given type var       */
  323.     Tyvar *tyv = tyvar(vn);
  324.  
  325.     if (tyv->bound)
  326.     return copyType(tyv->bound,tyv->offs);
  327.  
  328.     switch (tyv->offs) {
  329.     case FIXED_TYVAR    : return mkInt(vn);
  330.  
  331.     case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
  332.  
  333.     default         : return mkOffset(tyv->offs - GENERIC);
  334.     }
  335. }
  336.  
  337. static Type local copyType(t,o)            /* calculate most general form of  */
  338. Type t;                        /* type expression (t,o)        */
  339. Int  o; {
  340.     switch (whatIs(t)) {
  341.     case AP      : {   Type l = copyType(fst(t),o);  /* ensure correct */
  342.                Type r = copyType(snd(t),o);  /* eval. order    */
  343.                return ap(l,r);
  344.                }
  345.     case OFFSET  : return copyTyvar(o+offsetOf(t));
  346.     case INTCELL : return copyTyvar(intOf(t));
  347.     }
  348.  
  349.     return t;
  350. }
  351.  
  352. /* --------------------------------------------------------------------------
  353.  * Occurs check:
  354.  * ------------------------------------------------------------------------*/
  355.  
  356. static Tyvar *lookingFor;               /* var to look for in occurs check */
  357.  
  358. static Bool local doesntOccurIn(t,o)       /* Return TRUE if var lookingFor   */
  359. Type t;                        /* isn't referenced in (t,o)       */
  360. Int o; {
  361.     Tyvar *tyv;
  362.  
  363.     deRef(tyv,t,o);
  364.     if (tyv)                /* type variable           */
  365.         return tyv!=lookingFor;
  366.     if (isAp(t)) {            /* type constructor with args       */
  367.     Type t1 = t;
  368.         do {
  369.             if (doesntOccurIn(snd(t1),o))
  370.                 t1 = fst(t1);
  371.             else
  372.                 return FALSE;
  373.         } while (isAp(t1));
  374.     }
  375.     return TRUE;            /* variable was not found       */
  376. }
  377.  
  378. /* --------------------------------------------------------------------------
  379.  * Unification algorithm:
  380.  * ------------------------------------------------------------------------*/
  381.  
  382. static matchMode = FALSE;               /* set to TRUE to prevent binding  */
  383.                            /* during matching process       */
  384.  
  385. static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2       */
  386. Tyvar *tyv1, *tyv2; {
  387.     if (tyv1!=tyv2)
  388.     if (matchMode)
  389.         return FALSE;
  390.     else {
  391.         tyv1->bound = var;
  392.         tyv1->offs    = tyvNum(tyv2);
  393.     }
  394.     return TRUE;
  395. }
  396.  
  397. static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)       */
  398. Tyvar *tyv;
  399. Type  t;                /* guaranteed not to be a v'ble or */
  400. Int   o; {                /* have synonym as outermost constr*/
  401.     if (!matchMode) {
  402.     lookingFor = tyv;
  403.     if (doesntOccurIn(t,o)) {
  404.         tyv->bound = t;
  405.         tyv->offs  = o;
  406.         return TRUE;
  407.     }
  408.     }
  409.     return FALSE;    /* INFINITE TYPE (or failed match in matchMode)    */
  410. }
  411.  
  412. static Bool local unify(t1,o1,t2,o2)    /* Main unification routine       */
  413. Type t1,t2;                /* unify (t1,o1) with (t2,o2)       */
  414. Int  o1,o2; {
  415.     Tyvar *tyv1, *tyv2;
  416.  
  417.     deRef(tyv1,t1,o1);
  418.     deRef(tyv2,t2,o2);
  419.  
  420. un: if (tyv1)
  421.         if (tyv2)
  422.         return varToVarBind(tyv1,tyv2);        /* t1, t2 variables    */
  423.         else {
  424.             Cell h2 = getHead(t2);
  425.             if (isSynonym(h2)) {
  426.                 expandSynonym(h2,&t2,&o2);
  427.                 deRef(tyv2,t2,o2);
  428.                 goto un;
  429.             }
  430.         return varToTypeBind(tyv1,t2,o2);        /* t1 variable, t2 not */
  431.         }
  432.     else
  433.         if (tyv2) {
  434.             Cell h1 = getHead(t1);
  435.             if (isSynonym(h1)) {
  436.                 expandSynonym(h1,&t1,&o1);
  437.                 deRef(tyv1,t1,o1);
  438.                 goto un;
  439.             }
  440.         return varToTypeBind(tyv2,t1,o1);        /* t2 variable, t1 not */
  441.         }
  442.     else {                        /* t1, t2 not vars       */
  443.         Type h1 = getHead(t1);
  444.         Type h2 = getHead(t2);
  445.  
  446.         if (h1==h2) {               /* Assuming well-formed types, both*/
  447.         while (isAp(t1)) {         /* t1, t2 must have same no of args*/
  448.             if (!unify(arg(t1),o1,arg(t2),o2))
  449.             return FALSE;
  450.             t1 = fun(t1);
  451.             t2 = fun(t2);
  452.         }
  453.         return TRUE;
  454.         }
  455.  
  456.         /* Types do not match -- look for type synonyms to expand */
  457.  
  458.         if (isSynonym(h1)) {
  459.         expandSynonym(h1,&t1,&o1);
  460.         deRef(tyv1,t1,o1);
  461.         goto un;
  462.         }
  463.         if (isSynonym(h2)) {
  464.         expandSynonym(h2,&t2,&o2);
  465.                 deRef(tyv2,t2,o2);
  466.         goto un;
  467.         }
  468.     }
  469.     return FALSE;
  470. }
  471.  
  472. static Bool local sameType(t1,o1,t2,o2)/* Compare types without binding    */
  473. Type t1,t2;
  474. Int  o1,o2; {
  475.     Bool result;
  476.     matchMode = TRUE;
  477.     result    = unify(t1,o1,t2,o2);
  478.     matchMode = FALSE;
  479.     return result;
  480. }
  481.  
  482. Bool typeMatches(type,mt)        /* test if type matches monotype mt*/
  483. Type type, mt; {
  484.     Bool result;
  485.     if (isPolyType(type) || whatIs(type)==QUAL)
  486.     return FALSE;
  487.     typeChecker(RESET);
  488.     matchMode = TRUE;
  489.     result    = unify(mt,0,type,0);
  490.     matchMode = FALSE;
  491.     typeChecker(RESET);
  492.     return result;
  493. }
  494.  
  495. /* --------------------------------------------------------------------------
  496.  * Assumptions:
  497.  *
  498.  * A basic typing statement is a pair (Var,Type) and an assumption contains
  499.  * an ordered list of basic typing statements in which the type for a given
  500.  * variable is given by the most recently added assumption about that var.
  501.  *
  502.  * In practice, the assumption set is split between a pair of lists, one
  503.  * holding assumptions for vars defined in bindings, the other for vars
  504.  * defined in patterns/binding parameters etc.    The reason for this
  505.  * separation is that vars defined in bindings may be overloaded (with the
  506.  * overloading being unknown until the whole binding is typed), whereas the
  507.  * vars defined in patterns have no overloading.  A form of dependency
  508.  * analysis (at least as far as calculating dependents within the same group
  509.  * of value bindings) is required to implement this.  Where it is known that
  510.  * no overloaded values are defined in a binding (i.e. when the `dreaded
  511.  * monomorphism restriction' strikes), the list used to record dependents
  512.  * is flagged with a NODEPENDS tag to avoid gathering dependents at that
  513.  * level.
  514.  *
  515.  * To interleave between vars for bindings and vars for patterns, we use
  516.  * a list of lists of typing statements for each.  These lists are always
  517.  * the same length.  The implementation here is very similar to that of the
  518.  * dependency analysis used in the static analysis component of this system.
  519.  * ------------------------------------------------------------------------*/
  520.  
  521. static List defnBounds;                   /*::[[(Var,Type)]] possibly ovrlded*/
  522. static List varsBounds;                   /*::[[(Var,Type)]] not overloaded  */
  523. static List depends;                   /*::[?[Var]] dependents/NODEPENDS  */
  524.  
  525. #define saveVarsAssump() List saveAssump = hd(varsBounds)
  526. #define restoreVarsAss() hd(varsBounds)  = saveAssump
  527.  
  528. static Void local emptyAssumption() {      /* set empty type assumption       */
  529.     defnBounds = NIL;
  530.     varsBounds = NIL;
  531.     depends    = NIL;
  532. }
  533.  
  534. static Void local enterBindings() {    /* Add new level to assumption sets */
  535.     defnBounds = cons(NIL,defnBounds);
  536.     varsBounds = cons(NIL,varsBounds);
  537.     depends    = cons(NIL,depends);
  538. }
  539.  
  540. static Void local leaveBindings() {    /* Drop one level of assumptions    */
  541.     defnBounds = tl(defnBounds);
  542.     varsBounds = tl(varsBounds);
  543.     depends    = tl(depends);
  544. }
  545.  
  546. static Void local markAssumList(as)    /* Mark all types in assumption set */
  547. List as; {                   /* :: [(Var, Type)]           */
  548.     for (; nonNull(as); as=tl(as))     /* No need to mark generic types;   */
  549.     if (!isPolyType(snd(hd(as))))  /* the only free variables in those */
  550.         markType(snd(hd(as)),0);   /* must have been free earlier too  */
  551. }
  552.  
  553. static Cell local findAssum(t)           /* Find most recent assumption about*/
  554. Text t; {                   /* variable named t, if any       */
  555.     List defnBounds1 = defnBounds;     /* return translated variable, with */
  556.     List varsBounds1 = varsBounds;     /* type in typeIs           */
  557.     List depends1    = depends;
  558.  
  559.     while (nonNull(defnBounds1)) {
  560.     Pair ass = findInAssumList(t,hd(varsBounds1));/* search varsBounds */
  561.     if (nonNull(ass)) {
  562.         typeIs = snd(ass);
  563.         return fst(ass);
  564.     }
  565.  
  566.     ass = findInAssumList(t,hd(defnBounds1));     /* search defnBounds */
  567.     if (nonNull(ass)) {
  568.         Cell v = fst(ass);
  569.             typeIs = snd(ass);
  570.  
  571.         if (hd(depends1)!=NODEPENDS &&          /* save dependent?   */
  572.           isNull(v=varIsMember(t,hd(depends1))))
  573.         /* N.B. make new copy of variable and store this on list of*/
  574.         /* dependents, and in the assumption so that all uses of   */
  575.         /* the variable will be at the same node, if we need to    */
  576.         /* overwrite the call of a function with a translation...  */
  577.         hd(depends1) = cons(v=mkVar(t),hd(depends1));
  578.  
  579.         return v;
  580.     }
  581.  
  582.     defnBounds1 = tl(defnBounds1);              /* look in next level*/
  583.     varsBounds1 = tl(varsBounds1);              /* of assumption set */
  584.     depends1    = tl(depends1);
  585.     }
  586.     return NIL;
  587. }
  588.  
  589. static Pair local findInAssumList(t,as)/* Search for assumption for var    */
  590. Text t;                       /* named t in list of assumptions as*/
  591. List as; {
  592.     for (; nonNull(as); as=tl(as))
  593.     if (textOf(fst(hd(as)))==t)
  594.         return hd(as);
  595.     return NIL;
  596. }
  597.  
  598. #define findTopBinding(v)  findInAssumList(textOf(v),hd(defnBounds))
  599.  
  600. static Int local newVarsBind(v)        /* make new assump for pattern var  */
  601. Cell v; {
  602.     Int beta       = newTyvars(1);
  603.     hd(varsBounds) = cons(pair(v,mkInt(beta)), hd(varsBounds));
  604.     return beta;
  605. }
  606.  
  607. static Void local newDefnBind(v,type)  /* make new assump for defn var       */
  608. Cell v;                    /* and set type if given (nonNull)  */
  609. Type type; {
  610.     Int beta       = newTyvars(1);
  611.     hd(defnBounds) = cons(pair(v,mkInt(beta)), hd(defnBounds));
  612.     instantiate(type);
  613.     bind(beta,typeIs,typeOff);           /* Bind beta to new type skeleton   */
  614. }
  615.  
  616. static Void local instantiate(type)    /* instantiate type expr, if nonNull*/
  617. Type type; {
  618.     predsAre = NIL;
  619.     typeIs   = type;
  620.     typeOff  = 0;
  621.  
  622.     if (nonNull(typeIs)) {           /* instantiate type expression ?    */
  623.  
  624.     if (isPolyType(typeIs)) {      /* Polymorphic type scheme ?       */
  625.         typeOff = newTyvars(intOf(fst(typeIs)));
  626.         typeIs  = snd(typeIs);
  627.     }
  628.  
  629.     if (whatIs(typeIs)==QUAL) {    /* Qualified type?           */
  630.         predsAre = fst(snd(typeIs));
  631.         typeIs   = snd(snd(typeIs));
  632.     }
  633.     }
  634. }
  635.  
  636. /* --------------------------------------------------------------------------
  637.  * Predicate sets:
  638.  *
  639.  * A predicate set is represented by a list of triples (C t, o, used)
  640.  * which indicates that type (t,o) must be an instance of class C, with
  641.  * evidence required at the node pointed to by used.  Note that the `used'
  642.  * node may need to be overwritten at a later stage if this evidence is
  643.  * to be derived from some other predicates by entailment.
  644.  * ------------------------------------------------------------------------*/
  645.  
  646. #include "preds.c"
  647.  
  648. /* --------------------------------------------------------------------------
  649.  * Type errors:
  650.  * ------------------------------------------------------------------------*/
  651.  
  652. static Void local typeError(l,e,in,wh,t,o)
  653. Int    l;                  /* line number near type error       */
  654. String wh;                  /* place in which error occurs       */
  655. Cell   e;                  /* source of error           */
  656. Cell   in;                  /* context if any (NIL if not)       */
  657. Type   t;                  /* should be of type (t,o)       */
  658. Int    o; {                  /* type inferred is (typeIs,typeOff) */
  659.  
  660.     clearMarks();              /* types printed here are monotypes  */
  661.                       /* use marking to give sensible names*/
  662.  
  663.     ERROR(l) "Type error in %s", wh   ETHEN
  664.     if (nonNull(in)) {
  665.     ERRTEXT "\n*** expression     : " ETHEN ERREXPR(in);
  666.     }
  667.     ERRTEXT "\n*** term           : " ETHEN ERREXPR(e);
  668.     ERRTEXT "\n*** type           : " ETHEN ERRTYPE(copyType(typeIs,typeOff));
  669.     ERRTEXT "\n*** does not match : " ETHEN ERRTYPE(copyType(t,o));
  670.     ERRTEXT "\n"
  671.     EEND;
  672. }
  673.  
  674. #define shouldBe(l,e,in,where,t,o) if (!unify(typeIs,typeOff,t,o)) \
  675.                        typeError(l,e,in,where,t,o);
  676. #define check(l,e,in,where,t,o)    e=typeExpr(l,e); shouldBe(l,e,in,where,t,o)
  677. #define inferType(t,o)           typeIs=t; typeOff=o
  678.  
  679. /* --------------------------------------------------------------------------
  680.  * Typing of expressions:
  681.  * ------------------------------------------------------------------------*/
  682.  
  683. static patternMode = FALSE;           /* set to TRUE to type check pattern*/
  684.  
  685. static Cell local typeExpr(l,e)        /* Determine type of expr/pattern  */
  686. Int  l;
  687. Cell e; {
  688.     static String cond       = "conditional";
  689.     static String list       = "list";
  690.     static String listComp = "list comprehension";
  691.     static String discr    = "case discriminant";
  692.  
  693.     switch (whatIs(e)) {
  694.  
  695.     /* The following cases can occur in either pattern or expr. mode   */
  696.  
  697.     case AP     : return typeAp(l,e);
  698.  
  699.     case NAME    : if (isNull(name(e).type))
  700.                   internal("typeExpr1");
  701.               return varIntro(e,name(e).type);
  702.  
  703.     case TUPLE    : typeTuple(e);
  704.               break;
  705.  
  706.     case INTCELL    : if (!patternMode && coerceNumLiterals) {
  707.                   Int alpha = newTyvars(1);
  708.                   inferType(var,alpha);
  709.                   return ap(ap(nameFromInt,
  710.                        assumeEvid(predNum,alpha)),
  711.                        e);
  712.               }
  713.               else {
  714.                   inferType(typeInt,0);
  715.               }
  716.               break;
  717.  
  718.     case FLOATCELL  : inferType(typeFloat,0);
  719.               break;
  720.  
  721.     case STRCELL    : inferType(typeString,0);
  722.               break;
  723.  
  724.     case UNIT    : inferType(typeUnit,0);
  725.               break;
  726.  
  727.     case CHARCELL    : inferType(typeChar,0);
  728.               break;
  729.  
  730.     case VAROPCELL    :
  731.     case VARIDCELL    : if (patternMode) {
  732.                   inferType(var,newVarsBind(e));
  733.               }
  734.               else {
  735.                   Cell a = findAssum(textOf(e));
  736.                   if (nonNull(a))
  737.                   return varIntro(a,typeIs);
  738.                   else {
  739.                    a = findName(textOf(e));
  740.                    if (isNull(a) || isNull(name(a).type))
  741.                        internal("typeExpr2");
  742.                    return varIntro(a,name(a).type);
  743.                   }
  744.               }
  745.               break;
  746.  
  747.     /* The following cases can only occur in expr mode           */
  748.  
  749.     case COND    : {   Int beta = newTyvars(1);
  750.                   check(l,fst3(snd(e)),e,cond,typeBool,0);
  751.                   check(l,snd3(snd(e)),e,cond,var,beta);
  752.                   check(l,thd3(snd(e)),e,cond,var,beta);
  753.                   tyvarType(beta);
  754.               }
  755.               break;
  756.  
  757.     case FINLIST    : {   Int  beta = newTyvars(1);
  758.                   List xs;
  759.                   for (xs=snd(e); nonNull(xs); xs=tl(xs)) {
  760.                  check(l,hd(xs),e,list,var,beta);
  761.                   }
  762.                   inferType(typeList,beta);
  763.               }
  764.               break;
  765.  
  766.     case LETREC    : enterBindings();
  767.               mapProc(typeBindings,fst(snd(e)));
  768.               snd(snd(e)) = typeExpr(l,snd(snd(e)));
  769.               leaveBindings();
  770.               break;
  771.  
  772.     case LISTCOMP    : {   Int beta = newTyvars(1);
  773.                   saveVarsAssump();
  774.                   map1Proc(typeQualifier,l,snd(snd(e)));
  775.                   check(l,fst(snd(e)),NIL,listComp,var,beta);
  776.                   inferType(typeList,beta);
  777.                   restoreVarsAss();
  778.               }
  779.               break;
  780.  
  781.     case ESIGN    : typeEsign(l,e);
  782.               return fst(snd(e));
  783.  
  784.     case CASE    : {    Int beta = newTyvars(2);    /* discr result */
  785.                    check(l,fst(snd(e)),NIL,discr,var,beta);
  786.                    map2Proc(typeCase,l,beta,snd(snd(e)));
  787.                    tyvarType(beta+1);
  788.               }
  789.               break;
  790.  
  791.     case LAMBDA    : typeAlt(snd(e));
  792.               break;
  793.  
  794.     /* The remaining cases can only occur in pattern mode: */
  795.  
  796.     case WILDCARD    : inferType(var,newTyvars(1));
  797.               break;
  798.  
  799.     case ASPAT    : snd(snd(e)) = typeExpr(l,snd(snd(e)));
  800.               bind(newVarsBind(fst(snd(e))),typeIs,typeOff);
  801.               break;
  802.  
  803.     case LAZYPAT    : snd(e) = typeExpr(l,snd(e));
  804.               break;
  805.  
  806.     case ADDPAT    :
  807.     case MULPAT    : inferType(typeIntToInt,0);
  808.               break;
  809.  
  810.     default     : internal("typeExpr3");
  811.    }
  812.  
  813.    return e;
  814. }
  815.  
  816. static Cell local varIntro(v,type)     /* make translation of var v with   */
  817. Cell v;                       /* given type adding any extra dict */
  818. Type type; {                   /* params required           */
  819.     /* N.B. In practice, v will either be a NAME or a VARID/OPCELL       */
  820.     for (instantiate(type); nonNull(predsAre); predsAre=tl(predsAre))
  821.     v = ap(v,assumeEvid(hd(predsAre),typeOff));
  822.     return v;
  823. }
  824.  
  825. static Void local typeEsign(l,e)    /* Type check expression type sig  */
  826. Int  l;
  827. Cell e; {
  828.     static String typeSig = "type signature expression";
  829.     List savePreds = preds;
  830.     Int  alpha        = newTyvars(1);
  831.     List expPreds;            /* explicit preds in type sig       */
  832.     List qs;                /* qualifying preds in infered type*/
  833.     Type nt;                /* complete infered type       */
  834.  
  835.     preds = NIL;
  836.     instantiate(snd(snd(e)));
  837.     bind(alpha,typeIs,typeOff);
  838.     expPreds = makeEvidArgs(predsAre,typeOff);
  839.     check(l,fst(snd(e)),NIL,typeSig,var,alpha);
  840.  
  841.     clearMarks();
  842.     mapProc(markAssumList,defnBounds);
  843.     mapProc(markAssumList,varsBounds);
  844.     mapProc(markPred,savePreds);
  845.  
  846.     savePreds = elimConstPreds(l,typeSig,e,savePreds);
  847.  
  848.     explicitProve(l,typeSig,fst(snd(e)),expPreds,preds);
  849.  
  850.     resetGenericsFrom(0);
  851.     qs = copyPreds(expPreds);
  852.     nt = generalise(qs,copyTyvar(alpha));
  853.  
  854.     if (!equalSchemes(nt,snd(snd(e))))
  855.     tooGeneral(l,fst(snd(e)),snd(snd(e)),nt);
  856.  
  857.     tyvarType(alpha);
  858.     preds = revOnto(expPreds,savePreds);
  859. }
  860.  
  861. static Void local typeCase(l,beta,c)   /* type check case: pat -> rhs       */
  862. Int  l;                    /* (case given by c == (pat,rhs))   */
  863. Int  beta;                   /* need:  pat :: (var,beta)       */
  864. Cell c; {                   /*     rhs :: (var,beta+1)       */
  865.     static String casePat  = "case pattern";
  866.     static String caseExpr = "case expression";
  867.  
  868.     saveVarsAssump();
  869.  
  870.     fst(c) = typeFreshPat(l,fst(c));
  871.     shouldBe(l,fst(c),NIL,casePat,var,beta);
  872.     snd(c) = typeRhs(snd(c));
  873.     shouldBe(l,rhsExpr(snd(c)),NIL,caseExpr,var,beta+1);
  874.  
  875.     restoreVarsAss();
  876. }
  877.  
  878. static Void local typeQualifier(l,q)   /* type check qualifier in list comp*/
  879. Int  l;
  880. Cell q; {
  881.     static String boolQual = "boolean qualifier";
  882.     static String genQual  = "generator";
  883.     static String defnQual = "qualifier definition";
  884.  
  885.     switch (whatIs(q)) {
  886.     case BOOLQUAL : check(l,snd(q),NIL,boolQual,typeBool,0);
  887.             break;
  888.  
  889.     case QWHERE   : {   Int beta = newTyvars(1);
  890.                 fst(snd(q)) = typeFreshPat(l,fst(snd(q)));
  891.                 bind(beta,typeIs,typeOff);
  892.                 check(l,snd(snd(q)),NIL,defnQual,var,beta);
  893.             }
  894.             break;
  895.  
  896.     case FROMQUAL : {   Int beta = newTyvars(1);
  897.                 check(l,snd(snd(q)),NIL,genQual,typeList,beta);
  898.                 fst(snd(q)) = typeFreshPat(l,fst(snd(q)));
  899.                 shouldBe(l,fst(snd(q)),NIL,genQual,var,beta);
  900.             }
  901.             break;
  902.     }
  903. }
  904.  
  905. static Cell local typeFreshPat(l,p)    /* find type of pattern, assigning  */
  906. Int  l;                    /* fresh type variables to each var */
  907. Cell p; {                   /* bound in the pattern           */
  908.     patternMode = TRUE;
  909.     p         = typeExpr(l,p);
  910.     patternMode = FALSE;
  911.     return p;
  912. }
  913.  
  914. /* --------------------------------------------------------------------------
  915.  * Note the pleasing duality in the typing of application and abstraction:-)
  916.  * ------------------------------------------------------------------------*/
  917.  
  918. static Cell local typeAp(l,e)        /* Type check application       */
  919. Int  l;
  920. Cell e; {
  921.     static String app = "application";
  922.     Cell h    = getHead(e);        /* e = h e1 e2 ... en           */
  923.     Int  n    = argCount;        /* save no. of arguments       */
  924.     Int  beta = funcType(n);
  925.     Cell p    = NIL;            /* points to previous AP node       */
  926.     Cell a    = e;            /* points to current AP node       */
  927.     Int  i;
  928.  
  929.     check(l,h,e,app,var,beta);        /* check h::t1->t2->...->tn->rn+1  */
  930.     for (i=n; i>0; --i) {        /* check e_i::t_i for each i       */
  931.     check(l,arg(a),e,app,var,beta+2*i-1);
  932.     p = a;
  933.     a = fun(a);
  934.     }
  935.     fun(p) = h;                /* replace head with translation   */
  936.     tyvarType(beta+2*n);        /* inferred type is r_n+1       */
  937.     return e;
  938. }
  939.  
  940. static Void local typeAlt(a)        /* Type check abstraction (Alt)       */
  941. Cell a; {                /* a = ( [p1, ..., pn], rhs )       */
  942.     List ps      = fst(a);
  943.     Int  n      = length(ps);
  944.     Int  beta      = funcType(n);
  945.     Int  l      = rhsLine(snd(a));
  946.     Int  i;
  947.  
  948.     saveVarsAssump();
  949.  
  950.     for (i=0; i<n; ++i) {
  951.     hd(ps) = typeFreshPat(l,hd(ps));
  952.     bind(beta+2*i+1,typeIs,typeOff);
  953.     ps = tl(ps);
  954.     }
  955.     snd(a) = typeRhs(snd(a));
  956.     bind(beta+2*n,typeIs,typeOff);
  957.     tyvarType(beta);
  958.  
  959.     restoreVarsAss();
  960. }
  961.  
  962. static Int local funcType(n)        /*return skeleton for function type*/
  963. Int n; {                /*with n arguments, taking the form*/
  964.     Int beta = newTyvars(2*n+1);    /*    r1 t1 r2 t2 ... rn tn rn+1   */
  965.     Int i;                /* with r_i := t_i -> r_i+1       */
  966.     for (i=0; i<n; ++i)
  967.     bind(beta+2*i,arrow,beta+2*i+1);
  968.     return beta;
  969. }
  970.  
  971. /* --------------------------------------------------------------------------
  972.  * Tuple type constructors: are generated as necessary.  The most common
  973.  * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
  974.  * repeated generation of the constructor types.
  975.  *
  976.  * ???Maybe this cache should extend to all valid tuple constrs???
  977.  * ------------------------------------------------------------------------*/
  978.  
  979. #define MAXTUPCON 10
  980. static Type tupleConTypes[MAXTUPCON];
  981.  
  982. static Void local typeTuple(e)           /* find type for tuple constr, using*/
  983. Cell e; {                   /* tupleConTypes to cache previously*/
  984.     Int n   = tupleOf(e);           /* calculated tuple constr. types.  */
  985.     typeOff = newTyvars(n);
  986.     if (n>=MAXTUPCON)
  987.      typeIs = makeTupleType(n);
  988.     else if (tupleConTypes[n])
  989.      typeIs = tupleConTypes[n];
  990.     else
  991.      typeIs = tupleConTypes[n] = makeTupleType(n);
  992. }
  993.  
  994. static Type local makeTupleType(n)     /* construct type for tuple constr. */
  995. Int n; {                   /* t1 -> ... -> tn -> (t1,...,tn)   */
  996.     Type h = mkTuple(n);
  997.     Int  i;
  998.  
  999.     for (i=0; i<n; ++i)
  1000.     h = ap(h,mkOffset(i));
  1001.     while (0<n--)
  1002.     h = fn(mkOffset(n),h);
  1003.     return h;
  1004. }
  1005.  
  1006. /* --------------------------------------------------------------------------
  1007.  * Type check group of bindings:
  1008.  * ------------------------------------------------------------------------*/
  1009.  
  1010. static Void local typeBindings(bs)     /* type check a single binding group*/
  1011. List bs; {
  1012.     Bool usesPatternBindings = FALSE;
  1013.     Bool usesSimplePatterns  = FALSE;
  1014.     Bool usesTypeSigs = FALSE;
  1015.     List bs1;
  1016.  
  1017.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1)) {  /* Analyse binding group    */
  1018.     Cell b = hd(bs1);
  1019.     if (!isVar(fst(b)))
  1020.         usesPatternBindings = TRUE;
  1021.     else if (isNull(fst(hd(snd(snd(b))))))
  1022.         usesSimplePatterns = TRUE;
  1023.  
  1024.     if (nonNull(fst(snd(b))))           /* any explicitly typed       */
  1025.         usesTypeSigs = TRUE;           /* bindings in group?       */
  1026.     }
  1027.  
  1028.     hd(defnBounds) = NIL;
  1029.     hd(depends)       = NIL;
  1030.  
  1031.     if (usesPatternBindings || (usesSimplePatterns && !usesTypeSigs))
  1032.     noOverloading(bs);
  1033.     else if (usesTypeSigs)
  1034.     explicitTyping(bs);
  1035.     else
  1036.     implicitTyping(bs);
  1037.  
  1038.     mapProc(checkBindSigs,bs);               /* compare with sig decls   */
  1039.     mapProc(removeTypeSigs,bs);               /* Remove binding type info */
  1040.  
  1041.     hd(varsBounds) = revOnto(hd(defnBounds),   /* transfer completed assmps*/
  1042.                  hd(varsBounds));  /* out of defnBounds        */
  1043.     hd(defnBounds) = NIL;
  1044.     hd(depends)    = NIL;
  1045. }
  1046.  
  1047. static Void local removeTypeSigs(b)    /* Remove type info from a binding  */
  1048. Cell b; {
  1049.     snd(b) = snd(snd(b));
  1050. }
  1051.  
  1052. /* --------------------------------------------------------------------------
  1053.  * Restricted binding group:
  1054.  * ------------------------------------------------------------------------*/
  1055.  
  1056. static Void local noOverloading(bs)    /* Type restricted binding group    */
  1057. List bs; {
  1058.     List savePreds = preds;
  1059.     Cell v;
  1060.     Int  line;
  1061.  
  1062.     hd(depends) = NODEPENDS;           /* No need for dependents here       */
  1063.     preds       = NIL;
  1064.  
  1065.     mapProc(restrictedBindAss,bs);     /* add assumptions for vars in bs   */
  1066.     mapProc(typeBind,bs);           /* type check each binding       */
  1067.  
  1068.     clearMarks();               /* mark fixed variables           */
  1069.     mapProc(markAssumList,tl(defnBounds));
  1070.     mapProc(markAssumList,tl(varsBounds));
  1071.     mapProc(markPred,preds);
  1072.  
  1073.     if (isVar(v=fst(hd(bs))))
  1074.         line = rhsLine(snd(hd(snd(snd(hd(bs))))));
  1075.     else {
  1076.     line = rhsLine(snd(snd(snd(hd(bs)))));
  1077.     v    = hd(v);
  1078.     }
  1079.     savePreds = elimConstPreds(line,"binding group",v,savePreds);
  1080.     preds     = appendOnto(preds,savePreds);
  1081.  
  1082.     map2Proc(generaliseBind,0,NIL,bs); /* Generalise types of defined vars */
  1083. }
  1084.  
  1085. static Void local restrictedBindAss(b) /* make assums for vars in binding  */
  1086. Cell b; {                   /* gp with restricted overloading   */
  1087.  
  1088.     if (isVar(fst(b)))               /* function-binding?           */
  1089.     restrictedAss(intOf(rhsLine(snd(hd(snd(snd(b)))))),
  1090.               fst(b),
  1091.               fst(snd(b)));
  1092.     else {                   /* pattern-binding?           */
  1093.     List vs   = fst(b);
  1094.     List ts   = fst(snd(b));
  1095.     Int  line = rhsLine(snd(snd(b)));
  1096.  
  1097.     for (; nonNull(vs); vs=tl(vs))
  1098.         if (nonNull(ts)) {
  1099.         restrictedAss(line,hd(vs),hd(ts));
  1100.         ts = tl(ts);
  1101.         }
  1102.         else
  1103.         restrictedAss(line,hd(vs),NIL);
  1104.     }
  1105. }
  1106.  
  1107. static Void local restrictedAss(l,v,t) /* Assume that type of binding var v*/
  1108. Int  l;                    /* is t (if nonNull) in restricted  */
  1109. Cell v;                    /* binding group            */
  1110. Type t; {
  1111.     newDefnBind(v,t);
  1112.     if (nonNull(predsAre)) {
  1113.     ERROR(l) "Explicit overloaded type for \"%s\"",textToStr(textOf(v))
  1114.     ETHEN
  1115.     ERRTEXT  " not permitted in restricted binding"
  1116.     EEND;
  1117.     }
  1118. }
  1119.  
  1120. /* --------------------------------------------------------------------------
  1121.  * Type unrestricted binding group with explicitly declared types:
  1122.  * ------------------------------------------------------------------------*/
  1123.  
  1124. static Void local explicitTyping(bs)
  1125. List bs; {
  1126.     static String expBinds = "binding group";
  1127.     List savePreds  = preds;
  1128.     List evidParams = NIL;
  1129.     List locPreds   = NIL;
  1130.     List locDeps    = NIL;
  1131.     List bs1;
  1132.     List lps;
  1133.     List eps;
  1134.     Int  ng;
  1135.  
  1136.     preds = NIL;
  1137.  
  1138.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1)) {   /* Add assumptions about   */
  1139.     Cell b = hd(bs1);            /* each bound var -- can   */
  1140.     newDefnBind(fst(b),fst(snd(b)));    /* assume function binding */
  1141.     if (nonNull(typeIs))
  1142.         evidParams = cons(makeEvidArgs(predsAre,typeOff),evidParams);
  1143.     }
  1144.     evidParams    = rev(evidParams);
  1145.  
  1146.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1))    /* Type implicitly-typed   */
  1147.     if (isNull(fst(snd(hd(bs1)))))        /* function bindings       */
  1148.         typeBind(hd(bs1));
  1149.  
  1150.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1))    /* Type explicitly-typed   */
  1151.     if (nonNull(fst(snd(hd(bs1))))) {    /* binding and save local  */
  1152.         typeBind(hd(bs1));            /* dependents and preds       */
  1153.         locPreds    = cons(preds,locPreds);
  1154.         locDeps    = cons(hd(depends),locDeps);
  1155.         preds    = NIL;
  1156.         hd(depends) = NIL;
  1157.     }
  1158.     locPreds = rev(locPreds);
  1159.     locDeps  = rev(locDeps);
  1160.  
  1161.     /* ----------------------------------------------------------------------
  1162.      * At this point:
  1163.      *
  1164.      * bs         = group of bindings being typechecked
  1165.      * evidParams = list of explicit evidence parameters used in each
  1166.      *            explicitly typed binding in bs, arranged in the order
  1167.      *            that the explicitly typed bindings appear in bs.
  1168.      *            The first element of evidParams is also used as the
  1169.      *            explicit evidence parameters for any implicitly typed
  1170.      *            bindings in the group.
  1171.      * locPreds   = list of predicates required in the body of each
  1172.      *            explicitly typed binding in bs (arranged in the same
  1173.      *            order as evidParams.  Once again, the first element of
  1174.      *            locPreds also includes the predicates for the implicitly
  1175.      *            typed bindings in bs.
  1176.      * locDeps    = list of immediate dependents of each binding within the
  1177.      *            binding group bs.  Each of these variables must be
  1178.      *            overwritten with an expression in which the variable is
  1179.      *            applied to appropriate evidence parameters, as reqd by
  1180.      *            the corresponding element of evidParams.
  1181.      * --------------------------------------------------------------------*/
  1182.  
  1183.     clearMarks();                /* Mark fixed variables       */
  1184.     mapProc(markAssumList,tl(defnBounds));
  1185.     mapProc(markAssumList,tl(varsBounds));
  1186.     mapProc(markPred,savePreds);
  1187.  
  1188.     bs1 = gotoExplicit(bs);
  1189.     eps = evidParams;
  1190.     lps = locPreds;
  1191.     while (nonNull(eps)) {
  1192.     Cell b    = hd(bs1);
  1193.     Int  line = rhsLine(snd(hd(snd(snd(b)))));
  1194.     List dps;
  1195.  
  1196.     preds     = hd(lps);
  1197.     savePreds = elimConstPreds(line,expBinds,fst(b),savePreds);
  1198.  
  1199.     explicitProve(line,expBinds,fst(b),hd(eps),preds);
  1200.  
  1201.         for (dps=hd(locDeps); nonNull(dps); dps=tl(dps)) {
  1202.         Cell f      = hd(dps);
  1203.         Cell fQuals = explPreds(textOf(f),bs,evidParams);
  1204.  
  1205.         if (nonNull(fQuals))
  1206.                 overwrite(f,
  1207.               addEvidArgs(line,
  1208.                       expBinds,
  1209.                       fst(b),
  1210.                       hd(eps),
  1211.                       fQuals,
  1212.                       mkVar(textOf(f))));
  1213.     }
  1214.  
  1215.     eps       = tl(eps);
  1216.     bs1       = gotoExplicit(tl(bs));
  1217.     lps       = tl(lps);
  1218.     locDeps   = tl(locDeps);
  1219.     }
  1220.  
  1221.     eps = evidParams;                /* add extra dict params   */
  1222.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1)) {    /* to each binding in bs   */
  1223.     Cell b = hd(bs1);
  1224.  
  1225.     if (nonNull(fst(snd(b)))) {
  1226.         qualifyBinding(hd(eps),b);
  1227.         eps = tl(eps);
  1228.     }
  1229.     else
  1230.         qualifyBinding(hd(evidParams),b);
  1231.     }
  1232.  
  1233.     resetGenericsFrom(0);            /* Infer typing for each   */
  1234.     eps = copyPreds(hd(evidParams));        /* binding ....           */
  1235.     ng  = nextGeneric;
  1236.  
  1237.     for (bs1=bs; nonNull(bs1); bs1=tl(bs1))    /* Start with implicitly   */
  1238.     if (isNull(fst(snd(hd(bs1)))))        /* typed bindings       */
  1239.         generaliseBind(ng,eps,hd(bs1));
  1240.  
  1241.     bs1 = gotoExplicit(bs);            /* Then first explicitly   */
  1242.     generaliseBind(ng,eps,hd(bs1));        /* typed binding       */
  1243.  
  1244.     while (nonNull(bs1=gotoExplicit(tl(bs1)))) {/* followed by remaining   */
  1245.     evidParams = tl(evidParams);        /* explicitly typed bndings*/
  1246.         resetGenericsFrom(0);
  1247.     eps        = copyPreds(hd(evidParams));
  1248.     ng       = nextGeneric;
  1249.     generaliseBind(ng,eps,hd(bs1));
  1250.     }
  1251.  
  1252.     preds = savePreds;                /* restore saved predicates*/
  1253. }
  1254.  
  1255. static List local gotoExplicit(bs)      /* skip through list of bindings   */
  1256. List bs; {                /* upto first explicit binding       */
  1257.     while (nonNull(bs) && isNull(fst(snd(hd(bs)))))
  1258.     bs = tl(bs);
  1259.     return bs;
  1260. }
  1261.  
  1262. static List local explPreds(t,bs,locps)    /* look up explicit preds for t    in */
  1263. Text t;                     /* bindings bs with locps listing  */
  1264. List bs;                /* explicit type preds, implicit   */
  1265. List locps; {                /* included in hd(locps)       */
  1266.     List lps = locps;
  1267.  
  1268.     for (; nonNull(bs); bs=tl(bs)) {
  1269.     Cell b = hd(bs);
  1270.  
  1271.     if (textOf(fst(b))==t)
  1272.         if (isNull(fst(snd(b))))
  1273.         return hd(locps);
  1274.         else
  1275.         return hd(lps);
  1276.  
  1277.     if (nonNull(fst(snd(b))))
  1278.         lps = tl(lps);
  1279.     }
  1280.     internal("explPreds");
  1281.     return NIL; /*NOTREACHED*/
  1282. }
  1283.  
  1284. /* --------------------------------------------------------------------------
  1285.  * Type unrestricted binding group with no explicitly declared types:
  1286.  * ------------------------------------------------------------------------*/
  1287.  
  1288. static Void local implicitTyping(bs)
  1289. List bs; {
  1290.     static String impBinds = "implicitly typed binding group";
  1291.     Int  line      = rhsLine(snd(hd(snd(snd(hd(bs))))));
  1292.     Int  ng;
  1293.     List qs;
  1294.     List savePreds = preds;            /* Save and clear preds       */
  1295.     preds       = NIL;
  1296.  
  1297. #define addImplicit(b) newDefnBind(fst(b),NIL)    /* Add assumption for each */
  1298.     mapProc(addImplicit,bs);            /* variable defined in bs  */
  1299. #undef  addImplicit
  1300.  
  1301.     mapProc(typeBind,bs);            /* Type check each binding */
  1302.  
  1303.     clearMarks();                /* Mark fixed variables       */
  1304.     mapProc(markAssumList,tl(defnBounds));
  1305.     mapProc(markAssumList,tl(varsBounds));
  1306.     mapProc(markPred,savePreds);
  1307.  
  1308.     savePreds = elimConstPreds(line,
  1309.                    impBinds,
  1310.                    fst(hd(bs)),
  1311.                    savePreds);    /* remove (loc) const preds*/
  1312.     preds     = simplify(preds);        /* simplify remaining preds*/
  1313.     if (nonNull(preds)) {
  1314.     map1Proc(addEvidParams,preds,hd(depends));
  1315.     map1Proc(qualifyBinding,preds,bs);
  1316.     }
  1317.     resetGenericsFrom(0);
  1318.     qs = copyPreds(preds);
  1319.     ng = nextGeneric;
  1320.     map2Proc(generaliseBind,ng,qs,bs);        /* find defn var types     */
  1321.  
  1322.     preds = savePreds;                /* restore predicates       */
  1323. }
  1324.  
  1325. static Void local addEvidParams(qs,v)  /* overwrite VARID/OPCELL v with       */
  1326. List qs;                   /* application of variable to evid. */
  1327. Cell v; {                   /* parameters given by qs       */
  1328.     if (nonNull(qs)) {
  1329.     Cell nv;
  1330.  
  1331.     if (!isVar(v))
  1332.         internal("addEvidParams");
  1333.  
  1334.     for (nv=mkVar(textOf(v)); nonNull(tl(qs)); qs=tl(qs))
  1335.         nv = ap(nv,thd3(hd(qs)));
  1336.     fst(v) = nv;
  1337.     snd(v) = thd3(hd(qs));
  1338.     }
  1339. }
  1340.  
  1341. /* --------------------------------------------------------------------------
  1342.  * Type check bodies of class and instance declarations:
  1343.  * ------------------------------------------------------------------------*/
  1344.  
  1345. static Cell dictVar;            /* dict var used in inst/class defs*/
  1346.  
  1347. static Void local typeInstDefn(in)    /* type check implementations of   */
  1348. Inst in; {                /* member functions for instance in*/
  1349.     typeMembers("instance member binding",
  1350.         class(inst(in).cl).members,
  1351.         inst(in).implements,
  1352.         inst(in).head,
  1353.         inst(in).freedom);
  1354. }
  1355.  
  1356. static Void local typeClassDefn(c)    /* type check implementations of   */
  1357. Class c; {                /* defaults for class c           */
  1358.     typeMembers("default member binding",
  1359.         class(c).members,
  1360.         class(c).defaults,
  1361.         class(c).head,
  1362.         class(c).arity);
  1363. }
  1364.  
  1365. static Void local typeMembers(wh,ms,is,pi,ar)/* type check implementations */
  1366. String wh;                     /* `is' of members `ms' in    */
  1367. List   ms;                     /* class at instance `t' where*/
  1368. List   is;                     /* arity = #vars in t       */
  1369. Cell   pi;
  1370. Int    ar; {
  1371.     while (nonNull(is)) {
  1372.     if (isName(hd(is)))
  1373.         typeMember(wh,hd(ms),hd(is),pi,ar);
  1374.     is = tl(is);
  1375.     ms = tl(ms);
  1376.     }
  1377. }
  1378.  
  1379. static Void local typeMember(wh,m,i,pi,ar)   /* type check implementation i*/
  1380. String wh;                     /* of member m at instance t  */
  1381. Name   m;                     /* where arity = #vars in t   */
  1382. Name   i;
  1383. Cell   pi;
  1384. Int    ar; {
  1385.     Int  line = rhsLine(snd(hd(name(i).defn)));
  1386.     Int  alpha;
  1387.     Type rt = NIL;                /* required type       */
  1388.     Type it = NIL;                /* inferred type       */
  1389.     List evid;                    /* evidence assignment       */
  1390.     List qs;                    /* predicate list       */
  1391.  
  1392.     emptySubstitution();
  1393.     hd(defnBounds) = NIL;
  1394.     hd(depends)    = NODEPENDS;
  1395.     preds       = NIL;
  1396.  
  1397.     alpha = newTyvars(1+ar);
  1398.     instantiate(name(m).type);
  1399.     bind(alpha,typeIs,typeOff);
  1400.     if (isNull(predsAre) || !oneWayMatches(hd(predsAre),typeOff,pi,alpha+1))
  1401.     internal("typeMember1");
  1402.     evid = singleton(triple(hd(predsAre),mkInt(typeOff),dictVar));
  1403.  
  1404.     resetGenericsFrom(0);            /* Set required type, rt   */
  1405.     qs = copyPreds(evid);
  1406.     rt = generalise(qs,copyTyvar(alpha));
  1407.  
  1408.     map2Proc(typeDefAlt,alpha,m,name(i).defn);    /* Type each alt in defn   */
  1409.  
  1410.     if (nonNull(elimConstPreds(line,wh,m,NIL)))    /* need to resolve constant*/
  1411.     internal("typeMember2");        /* overloading - shouldn't */
  1412.                         /* be any locally constant */
  1413.                         /* overloading at all!       */
  1414.  
  1415.     explicitProve(line,wh,m,evid,preds);    /* resolve remaining preds */
  1416.  
  1417.     resetGenericsFrom(0);            /* Determine inferred type */
  1418.     qs = copyPreds(evid);
  1419.     it = generalise(qs,copyTyvar(alpha));
  1420.  
  1421.     if (!equalSchemes(rt,it))            /* check inferred type ok  */
  1422.     tooGeneral(line,m,rt,it);
  1423.  
  1424.     map1Proc(qualify,evid,name(i).defn);    /* add dictionary parameter*/
  1425.  
  1426.     overDefns = cons(i,overDefns);
  1427. }
  1428.  
  1429. /* --------------------------------------------------------------------------
  1430.  * Type check bodies of bindings:
  1431.  * ------------------------------------------------------------------------*/
  1432.  
  1433. static Void local typeBind(b)           /* Type check binding           */
  1434. Cell b; {
  1435.     if (isVar(fst(b))) {                   /* function binding */
  1436.     Cell ass = findTopBinding(fst(b));
  1437.     Int  beta;
  1438.  
  1439.     if (isNull(ass) || !isInt(snd(ass)))
  1440.         internal("typeBind");
  1441.  
  1442.     beta = intOf(snd(ass));
  1443.     map2Proc(typeDefAlt,beta,fst(b),snd(snd(b)));
  1444.     }
  1445.     else {                           /* pattern binding  */
  1446.     static String lhsPat = "lhs pattern";
  1447.     static String rhs    = "right hand side";
  1448.     Int  beta         = newTyvars(1);
  1449.     Pair pb             = snd(snd(b));
  1450.     Int  l             = rhsLine(snd(pb));
  1451.  
  1452.     check(l,fst(pb),NIL,lhsPat,var,beta);
  1453.     snd(pb) = typeRhs(snd(pb));
  1454.     shouldBe(l,rhsExpr(snd(pb)),NIL,rhs,var,beta);
  1455.     }
  1456. }
  1457.  
  1458. static Void local typeDefAlt(beta,v,a) /* type check alt in func. binding  */
  1459. Int  beta;
  1460. Cell v;
  1461. Pair a; {
  1462.     static String valDef = "function binding";
  1463.     Int l         = rhsLine(snd(a));
  1464.     typeAlt(a);
  1465.     shouldBe(l,v,NIL,valDef,var,beta);
  1466. }
  1467.  
  1468. static Cell local typeRhs(e)           /* check type of rhs of definition  */
  1469. Cell e; {
  1470.     switch (whatIs(e)) {
  1471.     case GUARDED : {   Int beta = newTyvars(1);
  1472.                map1Proc(guardedType,beta,snd(e));
  1473.                tyvarType(beta);
  1474.                }
  1475.                break;
  1476.  
  1477.     case LETREC  : enterBindings();
  1478.                mapProc(typeBindings,fst(snd(e)));
  1479.                snd(snd(e)) = typeRhs(snd(snd(e)));
  1480.                leaveBindings();
  1481.                break;
  1482.  
  1483.     default      : snd(e) = typeExpr(intOf(fst(e)),snd(e));
  1484.                break;
  1485.     }
  1486.     return e;
  1487. }
  1488.  
  1489. static Void local guardedType(beta,gded)/* check type of guard (li,(gd,ex))*/
  1490. Int  beta;                   /* should have gd :: Bool,       */
  1491. Cell gded; {                   /*          ex :: (var,beta)       */
  1492.     static String guarded = "guarded expression";
  1493.     static String guard   = "guard";
  1494.     Int line = intOf(fst(gded));
  1495.  
  1496.     gded     = snd(gded);
  1497.     check(line,fst(gded),NIL,guard,typeBool,0);
  1498.     check(line,snd(gded),NIL,guarded,var,beta);
  1499. }
  1500.  
  1501. Cell rhsExpr(rhs)               /* find first expression on a rhs   */
  1502. Cell rhs; {
  1503.     switch (whatIs(rhs)) {
  1504.     case GUARDED : return snd(snd(hd(snd(rhs))));
  1505.     case LETREC  : return rhsExpr(snd(snd(rhs)));
  1506.     default      : return snd(rhs);
  1507.     }
  1508. }
  1509.  
  1510. Int rhsLine(rhs)               /* find line number associated with */
  1511. Cell rhs; {                   /* a right hand side           */
  1512.     switch (whatIs(rhs)) {
  1513.     case GUARDED : return intOf(fst(hd(snd(rhs))));
  1514.     case LETREC  : return rhsLine(snd(snd(rhs)));
  1515.     default      : return intOf(fst(rhs));
  1516.     }
  1517. }
  1518.  
  1519. /* --------------------------------------------------------------------------
  1520.  * Calculate generalisation of types:
  1521.  * ------------------------------------------------------------------------*/
  1522.  
  1523. static Void local generaliseBind(ng,qs,b)
  1524. Int  ng;                               /* generalise the types of each var */
  1525. List qs;                   /* defined in binding, qualifying   */
  1526. Cell b; {                   /* with predicates in qs           */
  1527.     if (isVar(fst(b)))               /* Assumes fixed vars already marked*/
  1528.     generaliseAss(ng,qs,fst(b));   /* with first ng generics used in qs*/
  1529.     else {
  1530.     map2Proc(generaliseAss,ng,qs,fst(b));
  1531.     }
  1532. }
  1533.  
  1534. static Void local generaliseAss(ng,qs,v)/* Lookup type of var v in current */
  1535. Int  ng;                   /* top level assumptions and replace*/
  1536. List qs;                   /* by its generalisation, qualified */
  1537. Cell v; {                   /* by qs, first ng generics already */
  1538.     List ass = findTopBinding(v);      /* used.                   */
  1539.  
  1540.     if (isNull(ass) || !isInt(snd(ass)))
  1541.     internal("generaliseAss");
  1542.  
  1543.     resetGenericsFrom(ng);
  1544.     snd(ass) = generalise(qs,copyTyvar(intOf(snd(ass))));
  1545. }
  1546.  
  1547. static Type local generalise(qs,t)    /* calculate generalisation of t   */
  1548. List qs;                /* having already marked fixed vars*/
  1549. Type t; {                /* with qualifying preds qs       */
  1550.     if (nonNull(qs))
  1551.     t = ap(QUAL,pair(qs,t));
  1552.     if (nextGeneric>0)
  1553.     t = pair(mkInt(nextGeneric),t);
  1554.     return t;
  1555. }
  1556.  
  1557. /* --------------------------------------------------------------------------
  1558.  * Compare declared type schemes with inferred type schemes:
  1559.  * ------------------------------------------------------------------------*/
  1560.  
  1561. static Void local checkBindSigs(b)     /* check explicit type signature in */
  1562. Cell b; {                   /* binding with inferred type       */
  1563.     if (nonNull(fst(snd(b)))) {
  1564.     if (isVar(fst(b)))           /* function-binding?           */
  1565.         checkTypeSig(rhsLine(snd(hd(snd(snd(b))))),
  1566.              fst(b),
  1567.              fst(snd(b)));
  1568.     else {                   /* pattern-binding?           */
  1569.         List vs   = fst(b);
  1570.         List ts   = fst(snd(b));
  1571.         Int  line = rhsLine(snd(snd(b)));
  1572.  
  1573.         while (nonNull(vs) && nonNull(ts)) {
  1574.         if (nonNull(hd(ts)))
  1575.             checkTypeSig(line,hd(vs),hd(ts));
  1576.         vs = tl(vs);
  1577.         ts = tl(ts);
  1578.         }
  1579.     }
  1580.     }
  1581. }
  1582.  
  1583. static Void local checkTypeSig(l,v,t)  /* Compare explicit type scheme t   */
  1584. Int  l;                       /* declared for v with generalised  */
  1585. Cell v;                       /* type in current assumption       */
  1586. Type t; {
  1587.     Cell ass = findTopBinding(v);
  1588.  
  1589.     if (isNull(ass))
  1590.     internal("checkTypeSig");
  1591.  
  1592.     if (nonNull(t) && !equalSchemes(t,snd(ass)))
  1593.     tooGeneral(l,v,t,snd(ass));
  1594. }
  1595.  
  1596. static Void local tooGeneral(l,e,dt,it)    /* explicit type sig. too general  */
  1597. Int  l;
  1598. Cell e;
  1599. Type dt, it; {
  1600.     ERROR(l) "Declared type too general" ETHEN
  1601.     ERRTEXT  "\n*** Expression    : "     ETHEN ERREXPR(e);
  1602.     ERRTEXT  "\n*** Declared type : "     ETHEN ERRTYPE(dt);
  1603.     ERRTEXT  "\n*** Inferred type : "     ETHEN ERRTYPE(it);
  1604.     ERRTEXT  "\n"
  1605.     EEND;
  1606. }
  1607.  
  1608. /* --------------------------------------------------------------------------
  1609.  * Compare type schemes:
  1610.  * ------------------------------------------------------------------------*/
  1611.  
  1612. static Bool local equalSchemes(s1,s2)  /* Compare type schemes for equality*/
  1613. Type s1, s2; {
  1614.     Bool b1 = isPolyType(s1);
  1615.     Bool b2 = isPolyType(s2);
  1616.     if (b1 || b2) {
  1617.         if (b1 && b2 && intOf(fst(s1))==intOf(fst(s2))) {
  1618.             s1 = snd(s1);
  1619.             s2 = snd(s2);
  1620.         }
  1621.         else
  1622.             return FALSE;
  1623.     }
  1624.  
  1625.     b1 = (whatIs(s1)==QUAL);
  1626.     b2 = (whatIs(s2)==QUAL);
  1627.     if (b1 && b2 && equalQuals(fst(snd(s1)),fst(snd(s2)))) {
  1628.     s1 = snd(snd(s1));
  1629.     s2 = snd(snd(s2));
  1630.     }
  1631.     else if (b1 && !b2 && isNull(fst(snd(s1))))    /* maybe somebody gave an   */
  1632.     s1 = snd(snd(s1));            /* explicitly null context? */
  1633.     else if (!b1 && b2 && isNull(fst(snd(s2))))
  1634.     s2 = snd(snd(s2));
  1635.     else if (b1 || b2)
  1636.     return FALSE;
  1637.  
  1638.     return equalTypes(s1,s2);
  1639. }
  1640.  
  1641. static Bool local equalQuals(qs1,qs2)  /* Compare lists of qualifying preds*/
  1642. List qs1, qs2; {
  1643.     while (nonNull(qs1) && nonNull(qs2)) {        /* loop thru lists */
  1644.     Cell q1 = hd(qs1);
  1645.     Cell q2 = hd(qs2);
  1646.  
  1647.         while (isAp(q1) && isAp(q2)) {            /* loop thru args  */
  1648.         if (!equalTypes(arg(q1),arg(q2)))
  1649.         return FALSE;
  1650.         q1 = fun(q1);
  1651.         q2 = fun(q2);
  1652.     }
  1653.     if (q1!=q2)                    /* compare classes */
  1654.         return FALSE;
  1655.     qs1 = tl(qs1);
  1656.     qs2 = tl(qs2);
  1657.     }
  1658.     return isNull(qs1) && isNull(qs2);            /* compare lengths */
  1659. }
  1660.  
  1661. static Bool local equalTypes(t1,t2)    /* Compare simple types for equality*/
  1662. Type t1, t2; {
  1663.  
  1664. et: if (whatIs(t1)!=whatIs(t2))
  1665.     return FALSE;
  1666.  
  1667.     switch (whatIs(t1)) {
  1668.     case TYCON   :
  1669.     case OFFSET  :
  1670.     case TUPLE   : return t1==t2;
  1671.  
  1672.     case INTCELL : return intOf(t1)!=intOf(t2);
  1673.  
  1674.     case UNIT    :
  1675.     case ARROW   :
  1676.     case LIST    : return TRUE;
  1677.  
  1678.     case AP      : if (equalTypes(fun(t1),fun(t2))) {
  1679.                t1 = arg(t1);
  1680.                t2 = arg(t2);
  1681.                goto et;
  1682.                }
  1683.                        return FALSE;
  1684.  
  1685.     default      : internal("equalTypes");
  1686.     }
  1687.  
  1688.     return TRUE;/*NOTREACHED*/
  1689. }
  1690.  
  1691. /* --------------------------------------------------------------------------
  1692.  * Entry points to type checker:
  1693.  * ------------------------------------------------------------------------*/
  1694.  
  1695. Type typeCheckExp() {               /* Type check top level expression  */
  1696.     Type type;
  1697.     List qs;
  1698.  
  1699.     typeChecker(RESET);
  1700.     enterBindings();
  1701.  
  1702.     inputExpr = typeExpr(0,inputExpr);
  1703.     clearMarks();
  1704.     type = copyType(typeIs,typeOff);
  1705.     if (nonNull(elimConstPreds(0,"expression",inputExpr,NIL)))
  1706.     internal("typeCheckExp");
  1707.     preds = simplify(preds);
  1708.     qs    = copyPreds(preds);
  1709.     type  = generalise(qs,type);
  1710.     if (nonNull(preds)) {        /* qualify input expression with   */
  1711.     if (whatIs(inputExpr)!=LAMBDA)    /* additional dictionary params       */
  1712.         inputExpr = ap(LAMBDA,pair(NIL,pair(mkInt(0),inputExpr)));
  1713.     qualify(preds,snd(inputExpr));
  1714.     }
  1715.     typeChecker(RESET);
  1716.     return type;
  1717. }
  1718.  
  1719. Void typeCheckDefns() {            /* Type check top level bindings    */
  1720.     Target t  = length(valDefns) + length(instDefns) + length(classDefns);
  1721.     Target i  = 0;
  1722.     List   gs;
  1723.  
  1724.     typeChecker(RESET);
  1725.     enterBindings();
  1726.     setGoal("Type checking",t);
  1727.  
  1728.     for (gs=valDefns; nonNull(gs); gs=tl(gs)) {
  1729.     typeDefnGroup(hd(gs));
  1730.     soFar(i++);
  1731.     }
  1732.     for (gs=instDefns; nonNull(gs); gs=tl(gs)) {
  1733.     typeInstDefn(hd(gs));
  1734.     soFar(i++);
  1735.     }
  1736.     for (gs=classDefns; nonNull(gs); gs=tl(gs)) {
  1737.     typeClassDefn(hd(gs));
  1738.     soFar(i++);
  1739.     }
  1740.  
  1741.     typeChecker(RESET);
  1742.     done();
  1743. }
  1744.  
  1745. static Void local typeDefnGroup(bs)    /* type check group of value defns */
  1746. List bs; {                /* (one top level scc)           */
  1747.     List as;
  1748.  
  1749.     emptySubstitution();
  1750.     hd(defnBounds) = NIL;
  1751.     preds       = NIL;
  1752.     typeBindings(bs);            /* find types for vars in bindings */
  1753.  
  1754.     if (nonNull(preds)) {        /* look for unresolved overloading */
  1755.     Cell b    = hd(bs);
  1756.         Cell ass;
  1757.         Int  line;
  1758.         Cell v;
  1759.  
  1760.     preds = simplify(preds);    /* Simplify context first ...       */
  1761.  
  1762.         if (isVar(fst(b))) {        /* determine var name & line no.   */
  1763.         v    = fst(b);
  1764.         line = rhsLine(snd(hd(snd(b))));
  1765.     }
  1766.     else {
  1767.         v    = hd(fst(b));
  1768.         line = rhsLine(snd(snd(b)));
  1769.     }
  1770.         ass = findInAssumList(textOf(v),hd(varsBounds));
  1771.  
  1772.     ERROR(line) "Unresolved top-level overloading" ETHEN
  1773.         ERRTEXT     "\n*** Binding             : %s", textToStr(textOf(v))
  1774.         ETHEN
  1775.         if (nonNull(ass)) {
  1776.             ERRTEXT "\n*** Inferred type       : " ETHEN ERRTYPE(snd(ass));
  1777.         }
  1778.         ERRTEXT     "\n*** Outstanding context : " ETHEN
  1779.                                                ERRCONTEXT(copyPreds(preds));
  1780.         ERRTEXT     "\n"
  1781.     EEND;
  1782.     }
  1783.  
  1784.     for (as=hd(varsBounds); nonNull(as); as=tl(as)) {
  1785.     Cell a = hd(as);        /* add infered types to environment*/
  1786.     Name n = findName(textOf(fst(a)));
  1787.  
  1788.     if (isNull(n))
  1789.         internal("typeDefnGroup");
  1790.     if (catchAmbigs && isAmbiguous(snd(a)))
  1791.         ambigError(name(n).line,"inferred type",n,snd(a));
  1792.     name(n).type = snd(a);
  1793.     }
  1794.     hd(varsBounds) = NIL;
  1795. }
  1796.  
  1797. /* --------------------------------------------------------------------------
  1798.  * Type checker control:
  1799.  * ------------------------------------------------------------------------*/
  1800.  
  1801. Void typeChecker(what)
  1802. Int what; {
  1803.     Int i;
  1804.  
  1805.     switch (what) {
  1806.     case RESET   : patternMode = FALSE;
  1807.                matchMode   = FALSE;
  1808.                predProve   = NIL;
  1809.                instPred       = NIL;
  1810.                instExpr       = NIL;
  1811.                emptySubstitution();
  1812.                emptyAssumption();
  1813.                preds       = NIL;
  1814.                break;
  1815.  
  1816.     case MARK    : for (i=0; i<MAXTUPCON; ++i)
  1817.                mark(tupleConTypes[i]);
  1818.                for (i=0; i<numTyvars; ++i)
  1819.                mark(tyvars[i].bound);
  1820.                mark(typeIs);
  1821.                mark(predsAre);
  1822.                mark(defnBounds);
  1823.                mark(varsBounds);
  1824.                mark(depends);
  1825.                mark(preds);
  1826.                mark(dictVar);
  1827.                mark(predProve);
  1828.                mark(instPred);
  1829.                mark(instExpr);
  1830.                mark(arrow);
  1831.                mark(typeList);
  1832.                mark(typeIntToInt);
  1833.                mark(predNum);
  1834.                break;
  1835.  
  1836.     case INSTALL : typeChecker(RESET);
  1837.  
  1838.                for (i=0; i<MAXTUPCON; ++i)
  1839.                tupleConTypes[i] = NIL;
  1840.  
  1841.                dictVar      = inventDictVar();
  1842.  
  1843.                var        = mkOffset(0);
  1844.                arrow        = fn(var,mkOffset(1));
  1845.  
  1846.                typeList     = ap(LIST,var);
  1847.                nameNil        = addPrimCfun("[]",0,0,ap(mkInt(1),
  1848.                                   typeList));
  1849.                nameCons     = addPrimCfun(":",2,1,ap(mkInt(1),
  1850.                                  fn(var,
  1851.                                  fn(typeList,
  1852.                                 typeList))));
  1853.  
  1854.                typeUnit     = UNIT;
  1855.  
  1856.                typeBool     = addPrimTycon("Bool",0,0,NIL);
  1857.                nameFalse    = addPrimCfun("False",0,0,typeBool);
  1858.                nameTrue     = addPrimCfun("True",0,1,typeBool);
  1859.  
  1860.                typeInt        = addPrimTycon("Int",0,0,NIL);
  1861.                typeFloat    = addPrimTycon("Float",0,0,NIL);
  1862.  
  1863.                typeChar     = addPrimTycon("Char",0,0,NIL);
  1864.                typeString   = addPrimTycon("String",0,1,ap(LIST,
  1865.                                    typeChar));
  1866.                typeIntToInt = ap(ap(ARROW,typeInt),typeInt);
  1867.  
  1868.                typeDialogue = newTycon(findText("Dialogue"));
  1869.                nameFromInt  = newName(findText("fromInteger"));
  1870.                classNum     = newClass(findText("Num"));
  1871.  
  1872.                tycon(typeDialogue).defn = PREDEFINED;
  1873.                name(nameFromInt).defn   = PREDEFINED;
  1874.                class(classNum).head     = PREDEFINED;
  1875.  
  1876.                predNum      = ap(classNum,var);
  1877.  
  1878.                break;
  1879.     }
  1880. }
  1881.  
  1882. /*-------------------------------------------------------------------------*/
  1883.